Nuprl Lemma : sub-equality
11,40
postcript
pdf
T
:Type,
P
:(
T
),
i
,
u
:
T
. (
i
=
u
)
(
P
(
u
))
(
i
=
u
{
j
:
T
| {
j
:
T
|
P
(
j
)} } )
latex
ProofTree
Definitions
Type
,
t
T
,
s
=
t
,
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
:
A
.
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
P
Q
origin
T:Type, P:(T
), i, u:T. (i = u) 
(P(u)) (i = u 
{j:T| {j:T| P(j)} } )
T:Type, P:(T), i, u:T. (i = u) (P(u)) (i = u {j:T| {j:T| P(j)} } )
TB(x)x:A. B(x) Q